$\forall$$A$:Type, $B$:($A$$\rightarrow$Type). AtomFree(Type;$A$) $\Rightarrow$ AtomFree($A$$\rightarrow$Type;$B$) $\Rightarrow$ AtomFree(Type;$x$:$A$$\rightarrow$$B$($x$))